﻿using System;
using System.Collections.Generic;
using System.Linq.Expressions;
using System.Text;
using System.Threading.Tasks;
using Library.Logic;

namespace Library.Linq.Expressions
{
    public class QuantificationExpression : Expression
    {
        internal QuantificationExpression(Expression variable, Expression expression, Expression reasoner)
        {
            this.variable = variable;
            this.expression = expression;
            this.reasoner = reasoner;
        }

        Expression variable;
        Expression expression;
        Expression reasoner;

        public Expression Variable
        {
            get
            {
                return variable;
            }
        }
        public Expression Expression
        {
            get
            {
                return expression;
            }
        }
        public Expression Reasoner
        {
            get
            {
                return reasoner;
            }
        }

        public override ExpressionType NodeType
        {
            get
            {
                return ExpressionType.Extension;
            }
        }
        public override Type Type
        {
            get
            {
                return typeof(bool);
            }
        }
        public override bool CanReduce
        {
            get
            {
                return true;
            }
        }
    }

    public class ExistentialQuantificationExpression : QuantificationExpression
    {
        internal ExistentialQuantificationExpression(Expression variable, Expression expression, Expression reasoner)
            : base(variable, expression, reasoner) { }

        public override Expression Reduce()
        {
            return Expression.Call(null, Builtin.Reflection.Builtin_Exists_xer, Variable, Expression, Reasoner);
        }
    }

    public class UniqueQuantificationExpression : QuantificationExpression
    {
        internal UniqueQuantificationExpression(Expression variable, Expression expression, Expression reasoner)
            : base(variable, expression, reasoner) { }

        public override Expression Reduce()
        {
            return Expression.Call(null, Builtin.Reflection.Builtin_Unique_xer, Variable, Expression, Reasoner);
        }
    }

    public class UniversalQuantificationExpression : QuantificationExpression
    {
        internal UniversalQuantificationExpression(Expression variable, Expression expression, Expression reasoner)
            : base(variable, expression, reasoner) { }

        public override Expression Reduce()
        {
            return Expression.Call(null, Builtin.Reflection.Builtin_ForAll_xer, Variable, Expression, Reasoner);
        }
    }
}
